$a$ declared in $M$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\uparrow$fpf{-}dom(KindDeq; locl($a$); (($M$.2).1))